x, y:. x  y  (x  y) 

latex

Definitions	P & Q, P  Q, , P  Q, P  Q, Top, tt, if b then t else f fi , r - s, qpositive(r), t.2, t.1, r * s, r + s, q_le(r;s), qeq(r;s), , x f y, <+>, a  b, r  s, P  Q, t  T, x:A. B(x)
Lemmas	le wf, assert of eq int, assert of lt int, or functionality wrt iff, assert of bor, assert wf, iff transitivity, iff functionality wrt iff, isint-int